Nuprl Lemma : zero_ann_a
12,41
postcript
pdf
a
,
b
:
. ((
a
= 0)
(
b
= 0))
((
a
*
b
) = 0)
latex
ProofTree
Definitions
,
t
T
,
P
Q
,
P
Q
,
x
:
A
.
B
(
x
)
origin
a, b:
. ((a = 0) 
(b = 0)) 
((a * b) = 0)
a, b:. ((a = 0) (b = 0)) ((a * b) = 0)
T Q Qx:A. B(x)